Search Results

Documents authored by Vortmeier, Nils

Document
DOI: 10.4230/LIPIcs.CSL.2023.35
Dynamic Complexity of Regular Languages: Big Changes, Small Work

Authors: Felix Tschirbs, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
Whether a changing string is member of a certain regular language can be maintained in the DynFO framework of Patnaik and Immerman: after changing the symbol at one position of the string, a first-order update formula can express - using additionally stored information - whether the resulting string is in the regular language. We extend this and further known results by considering changes of many positions at once. We also investigate to which degree the obtained update formulas imply work-efficient parallel dynamic algorithms.
Cite as

Felix Tschirbs, Nils Vortmeier, and Thomas Zeume. Dynamic Complexity of Regular Languages: Big Changes, Small Work. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{tschirbs_et_al:LIPIcs.CSL.2023.35,
  author =	{Tschirbs, Felix and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Complexity of Regular Languages: Big Changes, Small Work}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.35},
  URN =		{urn:nbn:de:0030-drops-174963},
  doi =		{10.4230/LIPIcs.CSL.2023.35},
  annote =	{Keywords: dynamic descriptive complexity, regular languages, batch changes, work}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ICDT.2022
LIPIcs, Volume 220, ICDT 2022, Complete Volume

Authors: Dan Olteanu and Nils Vortmeier

Published in: LIPIcs, Volume 220, 25th International Conference on Database Theory (ICDT 2022)

Abstract
LIPIcs, Volume 220, ICDT 2022, Complete Volume
Cite as

25th International Conference on Database Theory (ICDT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 220, pp. 1-354, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Proceedings{olteanu_et_al:LIPIcs.ICDT.2022,
  title =	{{LIPIcs, Volume 220, ICDT 2022, Complete Volume}},
  booktitle =	{25th International Conference on Database Theory (ICDT 2022)},
  pages =	{1--354},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-223-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{220},
  editor =	{Olteanu, Dan and Vortmeier, Nils},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2022},
  URN =		{urn:nbn:de:0030-drops-158737},
  doi =		{10.4230/LIPIcs.ICDT.2022},
  annote =	{Keywords: LIPIcs, Volume 220, ICDT 2022, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ICDT.2022.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Dan Olteanu and Nils Vortmeier

Published in: LIPIcs, Volume 220, 25th International Conference on Database Theory (ICDT 2022)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

25th International Conference on Database Theory (ICDT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 220, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{olteanu_et_al:LIPIcs.ICDT.2022.0,
  author =	{Olteanu, Dan and Vortmeier, Nils},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{25th International Conference on Database Theory (ICDT 2022)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-223-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{220},
  editor =	{Olteanu, Dan and Vortmeier, Nils},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2022.0},
  URN =		{urn:nbn:de:0030-drops-158745},
  doi =		{10.4230/LIPIcs.ICDT.2022.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.122
Dynamic Complexity of Reachability: How Many Changes Can We Handle?

Authors: Samir Datta, Pankaj Kumar, Anish Mukherjee, Anuj Tawari, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
In 2015, it was shown that reachability for arbitrary directed graphs can be updated by first-order formulas after inserting or deleting single edges. Later, in 2018, this was extended for changes of size (log n)/(log log n), where n is the size of the graph. Changes of polylogarithmic size can be handled when also majority quantifiers may be used. In this paper we extend these results by showing that, for changes of polylogarithmic size, first-order update formulas suffice for maintaining (1) undirected reachability, and (2) directed reachability under insertions. For classes of directed graphs for which efficient parallel algorithms can compute non-zero circulation weights, reachability can be maintained with update formulas that may use "modulo 2" quantifiers under changes of polylogarithmic size. Examples for these classes include the class of planar graphs and graphs with bounded treewidth. The latter is shown here. As the logics we consider cannot maintain reachability under changes of larger sizes, our results are optimal with respect to the size of the changes.
Cite as

Samir Datta, Pankaj Kumar, Anish Mukherjee, Anuj Tawari, Nils Vortmeier, and Thomas Zeume. Dynamic Complexity of Reachability: How Many Changes Can We Handle?. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 122:1-122:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.ICALP.2020.122,
  author =	{Datta, Samir and Kumar, Pankaj and Mukherjee, Anish and Tawari, Anuj and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Complexity of Reachability: How Many Changes Can We Handle?}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{122:1--122:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.122},
  URN =		{urn:nbn:de:0030-drops-125291},
  doi =		{10.4230/LIPIcs.ICALP.2020.122},
  annote =	{Keywords: Dynamic complexity, reachability, complex changes}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.36
Dynamic Complexity Meets Parameterised Algorithms

Authors: Jonas Schmidt, Thomas Schwentick, Nils Vortmeier, Thomas Zeume, and Ioannis Kokkinis

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
Dynamic Complexity studies the maintainability of queries with logical formulas in a setting where the underlying structure or database changes over time. Most often, these formulas are from first-order logic, giving rise to the dynamic complexity class DynFO. This paper investigates extensions of DynFO in the spirit of parameterised algorithms. In this setting structures come with a parameter k and the extensions allow additional "space" of size f(k) (in the form of an additional structure of this size) or additional time f(k) (in the form of iterations of formulas) or both. The resulting classes are compared with their non-dynamic counterparts and other classes. The main part of the paper explores the applicability of methods for parameterised algorithms to this setting through case studies for various well-known parameterised problems.
Cite as

Jonas Schmidt, Thomas Schwentick, Nils Vortmeier, Thomas Zeume, and Ioannis Kokkinis. Dynamic Complexity Meets Parameterised Algorithms. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{schmidt_et_al:LIPIcs.CSL.2020.36,
  author =	{Schmidt, Jonas and Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas and Kokkinis, Ioannis},
  title =	{{Dynamic Complexity Meets Parameterised Algorithms}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{36:1--36:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.36},
  URN =		{urn:nbn:de:0030-drops-116792},
  doi =		{10.4230/LIPIcs.CSL.2020.36},
  annote =	{Keywords: Dynamic complexity, parameterised complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.37
Dynamic Complexity of Parity Exists Queries

Authors: Nils Vortmeier and Thomas Zeume

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
Given a graph whose nodes may be coloured red, the parity of the number of red nodes can easily be maintained with first-order update rules in the dynamic complexity framework DynFO of Patnaik and Immerman. Can this be generalised to other or even all queries that are definable in first-order logic extended by parity quantifiers? We consider the query that asks whether the number of nodes that have an edge to a red node is odd. Already this simple query of quantifier structure parity-exists is a major roadblock for dynamically capturing extensions of first-order logic. We show that this query cannot be maintained with quantifier-free first-order update rules, and that variants induce a hierarchy for such update rules with respect to the arity of the maintained auxiliary relations. Towards maintaining the query with full first-order update rules, it is shown that degree-restricted variants can be maintained.
Cite as

Nils Vortmeier and Thomas Zeume. Dynamic Complexity of Parity Exists Queries. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{vortmeier_et_al:LIPIcs.CSL.2020.37,
  author =	{Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Complexity of Parity Exists Queries}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{37:1--37:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.37},
  URN =		{urn:nbn:de:0030-drops-116805},
  doi =		{10.4230/LIPIcs.CSL.2020.37},
  annote =	{Keywords: Dynamic complexity, parity quantifier, arity hierarchy}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2018.120
Reachability and Distances under Multiple Changes

Authors: Samir Datta, Anish Mukherjee, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

Abstract
Recently it was shown that the transitive closure of a directed graph can be updated using first-order formulas after insertions and deletions of single edges in the dynamic descriptive complexity framework by Dong, Su, and Topor, and Patnaik and Immerman. In other words, Reachability is in DynFO. In this article we extend the framework to changes of multiple edges at a time, and study the Reachability and Distance queries under these changes. We show that the former problem can be maintained in DynFO(+, x) under changes affecting O({log n}/{log log n}) nodes, for graphs with n nodes. If the update formulas may use a majority quantifier then both Reachability and Distance can be maintained under changes that affect O(log^c n) nodes, for fixed c in N. Some preliminary results towards showing that distances are in DynFO are discussed.
Cite as

Samir Datta, Anish Mukherjee, Nils Vortmeier, and Thomas Zeume. Reachability and Distances under Multiple Changes. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 120:1-120:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.ICALP.2018.120,
  author =	{Datta, Samir and Mukherjee, Anish and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Reachability and Distances under Multiple Changes}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{120:1--120:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.120},
  URN =		{urn:nbn:de:0030-drops-91245},
  doi =		{10.4230/LIPIcs.ICALP.2018.120},
  annote =	{Keywords: dynamic complexity, reachability, distances, complex changes}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.98
A Strategy for Dynamic Programs: Start over and Muddle Through

Authors: Samir Datta, Anish Mukherjee, Thomas Schwentick, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
A strategy for constructing dynamic programs is introduced that utilises periodic computation of auxiliary data from scratch and the ability to maintain a query for a limited number of change steps. It is established that if some program can maintain a query for log n change steps after an AC^1-computable initialisation, it can be maintained by a first-order dynamic program as well, i.e., in DynFO. As an application, it is shown that decision and optimisation problems defined by monadic second-order (MSO) and guarded second-order logic (GSO) formulas are in DynFO, if only change sequences that produce graphs of bounded treewidth are allowed. To establish this result, Feferman-Vaught-type composition theorems for MSO and GSO are established that might be useful in their own right.
Cite as

Samir Datta, Anish Mukherjee, Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. A Strategy for Dynamic Programs: Start over and Muddle Through. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 98:1-98:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.ICALP.2017.98,
  author =	{Datta, Samir and Mukherjee, Anish and Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas},
  title =	{{A Strategy for Dynamic Programs: Start over and Muddle Through}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{98:1--98:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.98},
  URN =		{urn:nbn:de:0030-drops-74470},
  doi =		{10.4230/LIPIcs.ICALP.2017.98},
  annote =	{Keywords: dynamic complexity, treewidth, monadic second order logic}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2017.19
Dynamic Complexity under Definable Changes

Authors: Thomas Schwentick, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 68, 20th International Conference on Database Theory (ICDT 2017)

Abstract
This paper studies dynamic complexity under definable change operations in the DynFO framework by Patnaik and Immerman. It is shown that for changes definable by parameter-free first-order formulas, all (uniform) AC1 queries can be maintained by first-order dynamic programs. Furthermore, many maintenance results for single-tuple changes are extended to more powerful change operations: (1) The reachability query for undirected graphs is first-order maintainable under single tuple changes and first-order defined insertions, likewise the reachability query for directed acyclic graphs under quantifier-free insertions. (2) Context-free languages are first-order maintainable under \EFO-defined changes. These results are complemented by several inexpressibility results, for example, that the reachability query cannot be maintained by quantifier-free programs under definable, quantifier-free deletions.
Cite as

Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. Dynamic Complexity under Definable Changes. In 20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{schwentick_et_al:LIPIcs.ICDT.2017.19,
  author =	{Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Complexity under Definable Changes}},
  booktitle =	{20th International Conference on Database Theory (ICDT 2017)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-024-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{68},
  editor =	{Benedikt, Michael and Orsi, Giorgio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2017.19},
  URN =		{urn:nbn:de:0030-drops-70596},
  doi =		{10.4230/LIPIcs.ICDT.2017.19},
  annote =	{Keywords: dynamic descriptive complexity, SQL updates, dynamic programs}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2016.14
Dynamic Graph Queries

Authors: Pablo Muñoz, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 48, 19th International Conference on Database Theory (ICDT 2016)

Abstract
Graph databases in many applications - semantic web, transport or biological networks among others - are not only large, but also frequently modified. Evaluating graph queries in this dynamic context is a challenging task, as those queries often combine first-order and navigational features. Motivated by recent results on maintaining dynamic reachability, we study the dynamic evaluation of traditional query languages for graphs in the descriptive complexity framework. Our focus is on maintaining regular path queries, and extensions thereof, by first-order formulas. In particular we are interested in path queries defined by non-regular languages and in extended conjunctive regular path queries (which allow to compare labels of paths based on word relations). Further we study the closely related problems of maintaining distances in graphs and reachability in product graphs. In this preliminary study we obtain upper bounds for those problems in restricted settings, such as undirected and acyclic graphs, or under insertions only, and negative results regarding quantifier-free update formulas. In addition we point out interesting directions for further research.
Cite as

Pablo Muñoz, Nils Vortmeier, and Thomas Zeume. Dynamic Graph Queries. In 19th International Conference on Database Theory (ICDT 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 48, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{munoz_et_al:LIPIcs.ICDT.2016.14,
  author =	{Mu\~{n}oz, Pablo and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Dynamic Graph Queries}},
  booktitle =	{19th International Conference on Database Theory (ICDT 2016)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-002-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{48},
  editor =	{Martens, Wim and Zeume, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2016.14},
  URN =		{urn:nbn:de:0030-drops-57830},
  doi =		{10.4230/LIPIcs.ICDT.2016.14},
  annote =	{Keywords: Dynamic descriptive complexity, graph databases, graph products, reachability, path queries}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.308
Static Analysis for Logic-based Dynamic Programs

Authors: Thomas Schwentick, Nils Vortmeier, and Thomas Zeume

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
The goal of dynamic programs as introduced by Patnaik and Immerman (1994) is to maintain the result of a fixed query for an input database which is subject to tuple insertions and deletions. To this end such programs store an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. One of those auxiliary relations is supposed to store the answer to the query. Several static analysis problems can be associated to such dynamic programs. Is the answer relation of a given dynamic program always empty? Does a program actually maintain a query? That is, is the answer given of the program the same when an input database was reached by two different modification sequences? Even more, is the content of auxiliary relations independent of the modification sequence that lead to an input database? We study the algorithmic properties of those and similar static analysis problems. Since all these problems can easily be seen to be undecidable for full first-order programs, we examine the exact borderline for decidability for restricted programs. Our focus is on restricting the arity of the input databases as well as the auxiliary databases, and to restrict the use of quantifiers.
Cite as

Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. Static Analysis for Logic-based Dynamic Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 308-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{schwentick_et_al:LIPIcs.CSL.2015.308,
  author =	{Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Static Analysis for Logic-based Dynamic Programs}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{308--324},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.308},
  URN =		{urn:nbn:de:0030-drops-54221},
  doi =		{10.4230/LIPIcs.CSL.2015.308},
  annote =	{Keywords: Dynamic descriptive complexity, algorithmic problems, emptiness, history independence, consistency}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact